
Process calculi  are usually Turing complete and have an undecidable
bisimilarity (and barbed congruence). 
Subcalculi have been studied where bisimilarity becomes decidable but
then one loses Turing completeness. 
Examples are BPA and BPP (see, e.g., \citep{KuceraJ06}) and
CCS without restriction and relabeling \citep{ChristensenHM94}.
In this chapter we have shown that \hocore is 
a Turing complete formalism for which bisimilarity is
decidable. We do not know other concurrency formalisms where the same
happens. Other peculiarities of \ahopi\ are: 
\begin{enumerate}
\item it is higher-order, and contextual bisimilarities (barbed
  congruence) coincide  with higher-order bisimilarity (as well as
  with others, such as context and normal bisimilarities); and 
\item  it is asynchronous (in that there is no continuation underneath
  an output), yet asynchronous and synchronous bisimilarities coincide.
\end{enumerate}
 We do not know other non-trivial formalisms in which properties (1) or (2)
 hold (of course (1) makes sense only on higher-order models). 

We have also given an  axiomatization for bisimilarity. From this
we have derived polynomial upper bounds to the decidability of
bisimilarity. 
The axiomatization also intuitively explains why
 results
such as decidability, and the collapse of  many forms of bisimilarity, 
are possible even though \ahopi\ is Turing complete: the bisimilarity relation is  very
discriminating.   
\finish{DS: looks like a negative point for us, thus written...} 


%For the two main undecidability results we 
While in Chapter \ref{chap:core}
we have used encodings of  Minsky machines, %(MM)  
here we have used encodings of the  Post correspondence problem (PCP) for our undecidability results.
The encodings are tailored to analyze different problems:
undecidability of termination, and undecidability of bisimilarity  with %four
static restrictions. The PCP encoding is always
divergent, and therefore cannot be used to reason about termination.
On the other hand, the encoding of % MM 
Minsky machines would require at least one restriction for
each instruction of the machine, and therefore 
 would have given us a (much) worse result for static restrictions. 
% Also, we think that b
We find both encodings 
interesting: they 
show different ways to exploit higher-order communications for
modeling.

% The encoding of Turing complete models (such as Minsky and Random Access Machines, RAMs \cite{ShepherdsonS63}) 
% is a common proof technique 
% for carrying out expressiveness studies. % (see, e.g., \cite{BusiGZ03,BusiZ04,BusiGZ-TR}).
% %In fact, this is a rather widespread proof technique nowadays.
% Our encoding of Minsky machines into \ahopi resembles in structure those in  \cite{BusiGZ03,BusiGZ-TR}, where RAMs are used to 
% investigate the expressive power of restriction and replication in name-passing calculi, 
% and those in  \cite{BusiZ04}, where the impact of restriction and movement on
% the expressiveness of Ambient calculi is studied. The similarities can be
% explained by the fact that all the encodings share the same guiding principle: 
% representing counting as the nesting of suitable components.
% Those components are restricted names in CCS \cite{BusiGZ03,BusiGZ-TR}, 
% recursive definitions in $\pi$-calculus \cite{BusiGZ03}, 
% %chains of restricted names in   
% %\cite{BusiGZ03,BusiGZ-TR,BusiZ04}, enclosing 
% ambients themselves in Ambient calculus \cite{BusiZ04}, and higher-order messages in our case.
% Note that by combining our encoding with the one of higher-order $\pi$  into $\pi$-calculus in \cite{SaWabook}, 
% we obtain an encoding very similar to the one in \cite{BusiGZ03}.
% However, we do not know of other works 
% using Turing complete models for proving expressiveness results in the context of higher-order process calculi.
% As mentioned in the Introduction, the usual yardstick for comparison are first-order languages such as the $\pi$-calculus.
% A recent work in that direction is \cite{Mikkel08}, which  
% presents an encoding of the $\pi$-calculus into Homer, a higher-order process calculus with locations \cite{Mikkel04}.
% %Furthermore, r
% Reductions from the PCP to prove undecidability results have been used in other settings.
% %This approach has been used, f
% For instance, suitable reductions are used   
% in \cite{NielsenPV02} to show the undecidability of equivalences in timed concurrent constraint languages, and in
% \cite{CharatonikT01}
% to show undecidability of the model checking problem for the Ambient calculus without 
% restriction but with replication.
% 
% 


% (e.g., counters, choice for  MM, and data structures such as lists for  PCP).
%\finish{DS: last sentence above: cut?} 
%\finish{JP: I'd say so.} 

% For the static
% restrictions,
% we could have reused 
% the MM encoding,  but this 
%  would have given us a (much) worst result: 
%  it would have 
% required a number of restrictions that depends on the number of
% instructions, thus to have the undecidability result we would need
% enough instructions to encode a universal Minsky Machine. 
% \finish{Alan, please add the exact number}
% \finish{AS: I could not find the number of instructions for a MM with 2 registers. I don't think it's this important.}
% \finish{DS: i vaguely remember an email of yours with a number some
%   weeks aho} 
% On the other hand, the PCP encoding is not useful to prove undecidability
% of termination  since all the processes that we will define
% diverge. Also, we think that both the encodings are interesting, since
% they show different ways to exploit higher-order communications for
% modeling (e.g., counters, choice for  MM, and data structures such as lists for  PCP)..

%Finally 
We have shown that bisimilarity becomes undecidable with the
addition of four static restrictions. 
We do not know what happens with one, two, or three static restrictions.
We also do not know whether the results presented would hold when one
abstracts from $\tau$-actions  and moves to \emph{weak} equivalences.
The problem seems much harder;  it  reminds us of the situation for BPA
and BPP, where strong bisimilarity is  decidable  
%in polynomial time \finish{if the processes are normed??}  
but the decidability of weak
bisimilarity is a long-standing open problem (see, e.g., \citep{KuceraJ06}).
% 
% %{\small
% \paragraph{Acknowledgments.}
% %\thanks{
% This research was initiated by some remarks and email exchange
%  with Naoki Kobayashi.
% We also benefited from exchanges with Jes\'{u}s Aranda, 
% Cinzia Di Giusto, Maurizio Gabbrielli, 
% Anton\'in Ku\v{c}era, Sergue\"{i} Lenglet,
% Nobuko Yoshida,
% and Gianluigi Zavattaro, 
% and from   feedback from 
%  the users of the Moca and Concurrency mailing lists.
% %We are also grateful to the anonymous reviewers 
% %for their remarks and suggestions.
% %}